Skip to content

symbols-bar: optionally show labels and slightly tweak margins #8420

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Jul 11, 2025

Conversation

haraldschilly
Copy link
Contributor

@haraldschilly haraldschilly commented Jul 8, 2025

This either renders just the icons next to the menu, and also adjusts the margin such that all the icons are aligned, see below:

Screenshot from 2025-07-11 11-33-59

I've also added a context menu for quick access. The setting below is still there as before merging this with upstream.

Screenshot from 2025-07-11 11-31-20 Screenshot from 2025-07-11 11-31-00

This is the setting:

Screenshot from 2025-07-08 16-49-59

And this is similar to before 1c54e48

@williamstein
Copy link
Contributor

I merged your other PR and now this one has conflicts for all the translations.

@williamstein
Copy link
Contributor

Today I moved the toolbar to the same row as the menu bar, which Andrey kept requesting, and actually it feels pretty good. This is unfortunately inconsistent with this PR, since there's not really room for labels now.

@williamstein
Copy link
Contributor

What would make sense with this PR would be that when labels are enabled, then the entire toolbar moves back to where it was. Fortunately, this is relatively easy/natural, since it's all in the title bar react component (just lightly change where the bar is rendered).

@haraldschilly haraldschilly force-pushed the symbol-icons-configurable branch from 028c015 to 8698c4b Compare July 11, 2025 08:45
@haraldschilly haraldschilly force-pushed the symbol-icons-configurable branch from a04fdf6 to 190a01b Compare July 11, 2025 09:42
@haraldschilly haraldschilly marked this pull request as ready for review July 11, 2025 09:44
@williamstein williamstein merged commit be1518c into master Jul 11, 2025
3 checks passed
@williamstein
Copy link
Contributor

I merged this since it's clearly way better than not having it. However, there are still 3 issues, which need to get addressed:

#8438

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants